package at.tasat.cnf;

import java.util.HashSet;
import java.util.Set;

public final class Clause {

	private final int id;
	private final int[] literals;

	public Clause(int id, int... literals) {
		this.id = id;
		this.literals = literals.clone();
		assert isSane();
	}

	private boolean isSane() {
		Set<Integer> usedLiterals = new HashSet<Integer>();
		for (int literal : literals) {
			if (!Literal.isLiteral(literal) || !usedLiterals.add(literal)) {
				return false;
			}
		}
		return true;
	}

	public int getId() {
		return id;
	}

	public int getNumberOfLiterals() {
		return literals.length;
	}

	public int getLiteral(int index) {
		return literals[index];
	}

	// TODO use other datastructure for O(1) implementation (maybe Literal class)
	public int getLiteralOfVariable(int variableId) {
		assert Literal.isVariable(variableId);
		for (int i = 0; i < getNumberOfLiterals(); i++) {
			int literal = getLiteral(i);
			if (Literal.getVariableId(literal) == variableId) {
				return literal;
			}
		}
		return 0;
	}

	@Override
	public int hashCode() {
		return id;
	}

	@Override
	public String toString() {
		StringBuilder literalsBuilder = new StringBuilder();
		for (int literal : literals) {
			if (!Literal.getPhase(literal)) {
				literalsBuilder.append("!");
			}
			literalsBuilder.append(Literal.getVariableId(literal));
			literalsBuilder.append(' ');
		}
		return id + ": (" + literalsBuilder.toString().trim() + ')';
	}

}
